\documentclass[11pt, fleqn]{article}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{lipsum}
\usepackage{tabularx}
\usepackage{tikz}

\usetikzlibrary{shadows}
\usetikzlibrary{arrows}
\usetikzlibrary{positioning}



\begin{document}

\setlength{\parindent}{0 cm}

\title{Assignment 1}
\author{James Gregory 3288801 \and Huy Nguyen 3430069}
\date{\today}
\maketitle

\section*{Proposed Solution}

\subsection*{Counter Storage}

Our shared counter is stored twice in a single array of size $2*n$ bytes. Bytes $0 .. (n-1)$ store an "old" copy of the counter in descending order and bytes $n .. (2n-1)$ store a "new" copy in ascending order, like so
$$ b_{n-1} , .. , b_0 , B_0 , .. , B_{n-1}$$

\subsection*{Pseudo Code}
The writer thread has it's own local counter which it increments locally to determine the new value of each byte. It then updates the shared counter in descending order.
The reader threads have their own copy of this counter which they read into in ascending order.\\\\
\begin{tabularx}{\textwidth}{| X | X | }
\hline
\multicolumn{2}{|c|}{\textbf{Our Algorithm}} \\ \hline
\multicolumn{2}{|c|}{byte sc[2n]}\\ \hline
\multicolumn{1}{|c|}{\textbf{Reader}} & \multicolumn{1}{c|}{\textbf{Writer}} \\
\multicolumn{1}{|c|}{byte rlc[2n] , result[n]} & \multicolumn{1}{c|}{byte wlc[2n]} \\\hline
r1: for i = 0 .. (2n-1) 					& 	w1: increment( wlc ) \\
r2: \hspace{5 mm} rlc[i] $\leftarrow$ sc[i] 	&	w2:  for i = (2n-1) .. 0 \\
r3: deduce\_value (rlc) 				&	w3: \hspace{5 mm} sc[i] $\leftarrow$ wlc[i] \\\hline
\end{tabularx}
\\\\\\
Obviously the writer would not need its local counter to be of size $2n$ bytes but doing so will make our proof easier.
\subsection*{Assumptions}

\begin{itemize}
\item Reads and writes to individual bytes are atomic.
\item The macro $increment()$ at $w1$ does not alter the shared counter (sc).
\item At no point does the Reader thread alter the shared counter (sc).
\item The macro $deduce\_value()$ does not alter the readers' local counter (rlc).
\end{itemize}

\subsection*{Invariants}
In order to find a useful invariant we define the following function $$C : Byte \rightarrow \mathbb N$$ We can imagine this function as the correctness function, which given a byte as input returns which iteration of the writer last updated it (a correctness value). After the $x^{th}$ iteration of the writer finishes, $$C( sc[i] ) = x ,  \hspace{10 mm} \forall i \in \mathbb N \text{ where } 0 \leq i < n$$.
\\
From this definition we can gather the following invariants:
\begin{itemize}
\item $ \Upsilon : C(wlc[i]) \geq C(sc[j]) $ \hspace{10 mm} $ \forall i , j \in \mathbb N $ where $  i,j < 2n $ 
\\ Since the writer always updates its local counter before the shared counter.
\item $ \Phi : C(sc[i+k]) \geq C(sc[i]) $ \hspace{10 mm}  $ \forall i , k \in \mathbb N $ where $ i + k \leq 2n$
\\ Since the writer updates the shared counter in descending order.
\item $ \Psi : C(rlc[i]) \leq C(sc[i]) $ \hspace{10 mm} $ \forall i \in \mathbb N $ where $ i < 2n$
\\ Since the reader can not read a more correct value than what is actually there.
\end{itemize}
\subsection*{Transition Diagrams}

\begin{tikzpicture} [
		state/.style={circle, circular drop shadow, fill=white, draw},
		label/.style={draw=none, fill=none}, ->, thick,
		node distance = 4cm]

\node [label] (R) {Reader:};
\node [state] (r1) [right = 1cm of  R ] {r1};
\node [state] (r2) [right = 5cm of r1] {r2};
\node [state] (r3) [right = 2cm of r2] {r3};

\node [label] (W) [below = 5cm of R] {Writer:};
\node [state] (w1) [right = 1cm of  W ] {w1};
\node [state] (w2) [right = 2cm of w1] {w2};
\node [state] (w3) [right = 5cm of w2] {w3};
\node [state] (w4) [right = 1cm of w3] {w4};

\path [every node/.style={font=\sffamily\small}]
	(r1) edge [bend left] node [above] {$rlc[i] \leftarrow sc[i]$} (r2)
	(r2) edge [bend left] node [below] {$i < 2n \text{ ; } i\leftarrow i+1$} (r1)
	(r2) edge node [above] {$i = 2n$} (r3)
	
	(w1) edge node [above] {$ i \leftarrow 2n-1 $} (w2)
	(w2) edge [bend left] node [above] {$sc[i] \leftarrow wlc[i]$} (w3)
	(w3) edge [bend left] node [below] {$i > 0 \text{ ; } i \leftarrow i-1$} (w2)
	(w3) edge node [above] {$i = 0$} (w4);
\end{tikzpicture}

\subsection*{Precondition}
Before anything has been written to we say the correctness value for all bytes is 0.
\begin{itemize}
\item $\phi : C(sc[i]) = C(rlc[i]) = C(wlc[i]) = 0 \hspace{10 mm} \forall i \in \mathbb N \text{ where } 0 \leq i < 2n$
\end{itemize}

\subsection*{Assertion Network Q}
For the writer our at each location we assert the invariants $\Upsilon \wedge \Psi$ so we get induction and interference freedom for free. 
For the reader we need to show that, in order to deduce a correct read, the following property holds at r3:
 $$\psi : C(rlc[i]) \leq C(rlc[i+k]) \hspace{10 mm} \forall i, k \mathbb N \text{ where } i + k < 2n$$. The assertions are as follows:
 \begin{align}
 &Q_{r1} : C(rlc[i-1]) \leq C(sc[i]) \hspace{10 mm}\text{ where } i > 0 \\
 &Q_{r2} : C(rlc[i-1]) \leq C(rlc[i]) \hspace{10 mm}\text{ where } i > 0 \\
 &Q_{r3} : C(rlc[i-1] \leq C(rlc[i]) \hspace{10 mm} \forall i \in \mathbb N \text{ where } 0 < i < n 
 \end{align}
 For local induction we get:
 \begin{align*}
&r1 \rightarrow r2: \models C(rlc[i-1]) \leq C(sc[i]) \wedge (i \geq 0) \wedge (rlc[i] \leftarrow sc[i]) \Rightarrow Q_{r2} \\
&r2 \rightarrow r1: \models Q_{r2} \wedge (i \leftarrow i + 1) \Rightarrow Q_{r1} \text{ since } Q_{r1} \equiv \Psi \wedge \Phi \\
&r2 \rightarrow r3: \models (rlc[i-1] \leq rlc[i]) \wedge (i = 2n-1) \Rightarrow Q_{r3} 
 \end{align*}
And since our assertions are only dependent on invariants or local variables we get interference freedom for free.
Since $Q_{r3} \equiv  \psi$ we show that this property holds when the reader enters its $deduce\_value()$ macro. As this property is based only on local variables, we can view this property to be an invariant whilst the reader is deducing a value.

\subsection*{Deducing a Value}


Assume we have byte m is more significant than byte k. So our local copy of the counter would store two versions of each byte in the following order

$$ .. , b_m , .. b_k , .. , B_k , .. , B_m , .. $$ From $\psi$ we have shown that leftmost copies have an lower correctness (are older versions of this byte).
 \\
 
If a particular byte is to be changed by the writer , but we have the same value for each of our two copies , this means the correctness values for those two copies are the same.
 \\\\
 Now we can show that if we detect a change our two copies , that this is the most significant byte to be changed by the writer.
 Assume that we detect the change in byte k , but byte m is also to be changed but goes undetected.
 
 \begin{align*}
 b_m == B_m \wedge b_k != B_k \\
 \psi &\Rightarrow C(b_m) \leq C(b_k) \leq C(B_k) \leq(B_m) \\
 b_k != B_k &\Rightarrow C(b_k) < C(B_k) \\
 			&\Rightarrow C(b_m) != C(B_m) \\
b_m == B_m &\Rightarrow C(b_m) == C(B_m) \\
contradiction
\end{align*}
So we know that byte k is actually the most significant byte to change and are aware of its old value $b_k$. By using this value and maxing out all lower bytes (setting them to 255) we find a correct read as this is the largest (therefore most recent) possible value the counter had as it made the transition from $b_k$ to $B_k$.
\\
\\
If byte m is the most significant byte to be changed, but no changes are actually detected then
\begin{align*}
\psi &\Rightarrow C(b_m) \leq C(b_k) \leq C(B_k) \leq(B_m) \\
b_m == B_m &\Rightarrow C(b_m) == C(B_m) \\
&\Rightarrow C(b_m) == C(b_k) == C(B_k) == (B_m)
\end{align*}
So all bytes have the same correctness value, meaning they were the same at the correct time, which is obviously a correct read value.
\section*{Implementation}

We implement the algorithm in two different ways, using C and model it with promela. 

\subsection*{C code}
The C code uses a byte array, whose size is specified by the user, for the counter . The main method creates and start a writer thread and as many reader thread as specified by the user. The actual shared byte array will contain twice the number of bytes specified by the user. 

The writer thread holds a local copy of the counter, increments it and copy it to the shared counter using memcopy. This ensures that the bytes are written left to right. The writer constantly increment the byte array indefinitely or by the number of rounds specified by the user. To signal the writer has finished writing, it set a volatile flag 'done' to true. The writer, upon copying to the shared byte array, ensures that the counter bytes are written mirroring each other in the shared array.

The reader threads read the shared counter from right to left into its local copy. Each reader will continuously read until the global static 'done' flag is set. Each reader compares the mirroring bytes int the local copy. If it detects a byte at a position is different from its mirror copy, it knows the writer has changed the bytes while it is still reading. The reader automatically deduces the remaining bytes by accepting the right version, and 

\subsection*{Promela code}

The Promela code is greatly simplified from the C code to reduce the number of state spaces. Instead of using bytes for counter, we uses bits. Furthermore we use only a single reader, a writer with and 8 bit array to simulate a 4-bit counter.

Similar to the C code, the promela writer has its own copy and updates the shared bit array each increment. Each bit updated right to left. The writer also update a global shared byte (current_val) that represents the 4-bit counter. This allows us to write linear(ltl) temporal logic assertions.

The reader copies the shared bit array from left to right to its local copy. It also reads the global shared byte before (lo) and after (hi) the the copying. This allow us to write further ltl assertions on the correctness of the reading. Like the C code, the reader also deduces the counter based upon the bit array. It publishes this result to a global variable (reader_val) for ltl assertions.

There are a number of d_step and atomic blocks throughout the promela code. This is done only on manipulation of local variables to reduce the number of state space in spin.

\section*{Verification}
\subsection*{Limitations of Spin}
One possible method to verify our solution would be to model our correctness function in spin and verify our proposed invariants. However, in the case where the writer loops indefinitely, the correctness value must also be able to increase indefinitely, which is definitely not possible. 

The file "psi.pml" is a modification of the problem, where instead of storing the counter values in the shared counter, we store the correctness value. There are 3 \#defines used to set the number of counter bytes, the number of readers and the maximum number of iterations. 



\end{document}